(set-logic QF_UF)
(set-info :source |
CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC
 for more information. 

This benchmark was obtained by trying to find a finite model of a first-order 
formula (Albert Oliveras).
|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-sort U 0)
(declare-fun c14 () U)
(declare-fun c12 () U)
(declare-fun p4 (U U) Bool)
(declare-fun c13 () U)
(declare-fun p3 (U U) Bool)
(declare-fun c15 () U)
(declare-fun c17 () U)
(declare-fun p6 (U U) Bool)
(declare-fun p2 (U U) Bool)
(declare-fun p1 (U U) Bool)
(declare-fun c11 () U)
(declare-fun f5 (U U) U)
(declare-fun c10 () U)
(declare-fun p8 (U) Bool)
(declare-fun c16 () U)
(declare-fun p9 (U U) Bool)
(declare-fun p7 (U U) Bool)
(declare-fun c_0 () U)
(declare-fun c_1 () U)
(declare-fun c_2 () U)
(declare-fun c_3 () U)
(declare-fun b0 () Bool)
(assert (let ((?v_52 (= c_0 c_0))) (let ((?v_16 (not ?v_52)) (?v_32 (p3 c_0 c_0)) (?v_55 (= c_0 c_1))) (let ((?v_17 (not ?v_55)) (?v_33 (p3 c_0 c_1)) (?v_58 (= c_0 c_2))) (let ((?v_18 (not ?v_58)) (?v_34 (p3 c_0 c_2)) (?v_61 (= c_0 c_3))) (let ((?v_19 (not ?v_61)) (?v_35 (p3 c_0 c_3)) (?v_64 (= c_1 c_0))) (let ((?v_20 (not ?v_64)) (?v_36 (p3 c_1 c_0)) (?v_67 (= c_1 c_1))) (let ((?v_21 (not ?v_67)) (?v_37 (p3 c_1 c_1)) (?v_70 (= c_1 c_2))) (let ((?v_22 (not ?v_70)) (?v_38 (p3 c_1 c_2)) (?v_73 (= c_1 c_3))) (let ((?v_23 (not ?v_73)) (?v_39 (p3 c_1 c_3)) (?v_76 (= c_2 c_0))) (let ((?v_24 (not ?v_76)) (?v_40 (p3 c_2 c_0)) (?v_79 (= c_2 c_1))) (let ((?v_25 (not ?v_79)) (?v_41 (p3 c_2 c_1)) (?v_82 (= c_2 c_2))) (let ((?v_26 (not ?v_82)) (?v_42 (p3 c_2 c_2)) (?v_85 (= c_2 c_3))) (let ((?v_27 (not ?v_85)) (?v_43 (p3 c_2 c_3)) (?v_88 (= c_3 c_0))) (let ((?v_28 (not ?v_88)) (?v_44 (p3 c_3 c_0)) (?v_91 (= c_3 c_1))) (let ((?v_29 (not ?v_91)) (?v_45 (p3 c_3 c_1)) (?v_94 (= c_3 c_2))) (let ((?v_30 (not ?v_94)) (?v_46 (p3 c_3 c_2)) (?v_97 (= c_3 c_3))) (let ((?v_31 (not ?v_97)) (?v_47 (p3 c_3 c_3)) (?v_53 (p4 c_0 c_0))) (let ((?v_0 (not ?v_53)) (?v_56 (p4 c_0 c_1))) (let ((?v_2 (not ?v_56)) (?v_65 (p4 c_1 c_0))) (let ((?v_1 (not ?v_65)) (?v_59 (p4 c_0 c_2))) (let ((?v_5 (not ?v_59)) (?v_77 (p4 c_2 c_0))) (let ((?v_4 (not ?v_77)) (?v_62 (p4 c_0 c_3))) (let ((?v_10 (not ?v_62)) (?v_89 (p4 c_3 c_0))) (let ((?v_9 (not ?v_89)) (?v_68 (p4 c_1 c_1))) (let ((?v_3 (not ?v_68)) (?v_71 (p4 c_1 c_2))) (let ((?v_7 (not ?v_71)) (?v_80 (p4 c_2 c_1))) (let ((?v_6 (not ?v_80)) (?v_74 (p4 c_1 c_3))) (let ((?v_12 (not ?v_74)) (?v_92 (p4 c_3 c_1))) (let ((?v_11 (not ?v_92)) (?v_83 (p4 c_2 c_2))) (let ((?v_8 (not ?v_83)) (?v_86 (p4 c_2 c_3))) (let ((?v_14 (not ?v_86)) (?v_95 (p4 c_3 c_2))) (let ((?v_13 (not ?v_95)) (?v_98 (p4 c_3 c_3))) (let ((?v_15 (not ?v_98)) (?v_54 (p2 c_0 c_0)) (?v_66 (p2 c_1 c_0)) (?v_78 (p2 c_2 c_0)) (?v_90 (p2 c_3 c_0)) (?v_57 (p2 c_0 c_1)) (?v_69 (p2 c_1 c_1)) (?v_81 (p2 c_2 c_1)) (?v_93 (p2 c_3 c_1)) (?v_60 (p2 c_0 c_2)) (?v_72 (p2 c_1 c_2)) (?v_84 (p2 c_2 c_2)) (?v_96 (p2 c_3 c_2)) (?v_63 (p2 c_0 c_3)) (?v_75 (p2 c_1 c_3)) (?v_87 (p2 c_2 c_3)) (?v_99 (p2 c_3 c_3)) (?v_100 (p1 c_0 c_0)) (?v_101 (p1 c_0 c_1)) (?v_102 (p1 c_0 c_2)) (?v_103 (p1 c_0 c_3)) (?v_104 (p1 c_1 c_0)) (?v_105 (p1 c_1 c_1)) (?v_106 (p1 c_1 c_2)) (?v_107 (p1 c_1 c_3)) (?v_108 (p1 c_2 c_0)) (?v_109 (p1 c_2 c_1)) (?v_110 (p1 c_2 c_2)) (?v_111 (p1 c_2 c_3)) (?v_112 (p1 c_3 c_0)) (?v_113 (p1 c_3 c_1)) (?v_114 (p1 c_3 c_2)) (?v_115 (p1 c_3 c_3)) (?v_117 (f5 c_0 c_0)) (?v_48 (not (p8 c_0))) (?v_116 (p6 c_0 c_0)) (?v_119 (f5 c_0 c_1)) (?v_118 (p6 c_0 c_1)) (?v_121 (f5 c_0 c_2)) (?v_120 (p6 c_0 c_2)) (?v_123 (f5 c_0 c_3)) (?v_122 (p6 c_0 c_3)) (?v_125 (f5 c_1 c_0)) (?v_49 (not (p8 c_1))) (?v_124 (p6 c_1 c_0)) (?v_127 (f5 c_1 c_1)) (?v_126 (p6 c_1 c_1)) (?v_129 (f5 c_1 c_2)) (?v_128 (p6 c_1 c_2)) (?v_131 (f5 c_1 c_3)) (?v_130 (p6 c_1 c_3)) (?v_133 (f5 c_2 c_0)) (?v_50 (not (p8 c_2))) (?v_132 (p6 c_2 c_0)) (?v_135 (f5 c_2 c_1)) (?v_134 (p6 c_2 c_1)) (?v_137 (f5 c_2 c_2)) (?v_136 (p6 c_2 c_2)) (?v_139 (f5 c_2 c_3)) (?v_138 (p6 c_2 c_3)) (?v_141 (f5 c_3 c_0)) (?v_51 (not (p8 c_3))) (?v_140 (p6 c_3 c_0)) (?v_143 (f5 c_3 c_1)) (?v_142 (p6 c_3 c_1)) (?v_145 (f5 c_3 c_2)) (?v_144 (p6 c_3 c_2)) (?v_147 (f5 c_3 c_3)) (?v_146 (p6 c_3 c_3))) (let ((?v_148 (not ?v_54)) (?v_152 (not ?v_66)) (?v_156 (not ?v_78)) (?v_160 (not ?v_90)) (?v_149 (not ?v_57)) (?v_153 (not ?v_69)) (?v_157 (not ?v_81)) (?v_161 (not ?v_93)) (?v_150 (not ?v_60)) (?v_154 (not ?v_72)) (?v_158 (not ?v_84)) (?v_162 (not ?v_96)) (?v_151 (not ?v_63)) (?v_155 (not ?v_75)) (?v_159 (not ?v_87)) (?v_163 (not ?v_99)) (?v_164 (p9 c_0 c_0))) (let ((?v_212 (not ?v_164)) (?v_196 (p7 c_0 c_0))) (let ((?v_165 (not ?v_196)) (?v_166 (p9 c_0 c_1))) (let ((?v_213 (not ?v_166)) (?v_197 (p7 c_0 c_1))) (let ((?v_167 (not ?v_197)) (?v_168 (p9 c_0 c_2))) (let ((?v_214 (not ?v_168)) (?v_198 (p7 c_0 c_2))) (let ((?v_169 (not ?v_198)) (?v_170 (p9 c_0 c_3))) (let ((?v_215 (not ?v_170)) (?v_199 (p7 c_0 c_3))) (let ((?v_171 (not ?v_199)) (?v_172 (p9 c_1 c_0))) (let ((?v_216 (not ?v_172)) (?v_200 (p7 c_1 c_0))) (let ((?v_173 (not ?v_200)) (?v_174 (p9 c_1 c_1))) (let ((?v_217 (not ?v_174)) (?v_201 (p7 c_1 c_1))) (let ((?v_175 (not ?v_201)) (?v_176 (p9 c_1 c_2))) (let ((?v_218 (not ?v_176)) (?v_202 (p7 c_1 c_2))) (let ((?v_177 (not ?v_202)) (?v_178 (p9 c_1 c_3))) (let ((?v_219 (not ?v_178)) (?v_203 (p7 c_1 c_3))) (let ((?v_179 (not ?v_203)) (?v_180 (p9 c_2 c_0))) (let ((?v_220 (not ?v_180)) (?v_204 (p7 c_2 c_0))) (let ((?v_181 (not ?v_204)) (?v_182 (p9 c_2 c_1))) (let ((?v_221 (not ?v_182)) (?v_205 (p7 c_2 c_1))) (let ((?v_183 (not ?v_205)) (?v_184 (p9 c_2 c_2))) (let ((?v_222 (not ?v_184)) (?v_206 (p7 c_2 c_2))) (let ((?v_185 (not ?v_206)) (?v_186 (p9 c_2 c_3))) (let ((?v_223 (not ?v_186)) (?v_207 (p7 c_2 c_3))) (let ((?v_187 (not ?v_207)) (?v_188 (p9 c_3 c_0))) (let ((?v_224 (not ?v_188)) (?v_208 (p7 c_3 c_0))) (let ((?v_189 (not ?v_208)) (?v_190 (p9 c_3 c_1))) (let ((?v_225 (not ?v_190)) (?v_209 (p7 c_3 c_1))) (let ((?v_191 (not ?v_209)) (?v_192 (p9 c_3 c_2))) (let ((?v_226 (not ?v_192)) (?v_210 (p7 c_3 c_2))) (let ((?v_193 (not ?v_210)) (?v_194 (p9 c_3 c_3))) (let ((?v_227 (not ?v_194)) (?v_211 (p7 c_3 c_3))) (let ((?v_195 (not ?v_211))) (or (?v_52 b0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
